'''
Created on 2011-04-10

@author: kacper
'''
from parsing.parser import sents_parse, sents_parse_string, theory_id
import sys
from dataStructs.Transform import cnf, MultipleAnd, MultipleOr, MultipleToList
from dataStructs.definitions import Default, Formula, NotFormula, Relation,\
    Const
from resolution.resolution import linearResolution
import resolution
import subprocess
from sets import Set
from copy import deepcopy
import copy

'''
class Axioms:
    pass

class Facts:
    pass

class Rules:
    pass
    
class Defaults:
        pass
''' 


def normalize(theory):
    if not isinstance(theory, list):
        theory = [theory] 
    return map(lambda x: x.removeThen().pushNeg(),theory )
        
def convertToCNF( theory):
    theory = normalize(theory)
    return   map( lambda x: cnf(x),theory )
    

        
def covertToList (x):
            if isinstance(x, Default): 
                return [MultipleToList(x.f2),MultipleToList(x.f1)]
            return [MultipleToList(x),[[]]]
        
        
def resolutionForm( theory):
    tmp = convertToCNF(theory)
    #for x in tmp: print x, MultipleToList(x)
    
    tmp =  map(lambda x: covertToList(x), tmp)
    #for x in tmp: print x

        
    def incConclusion(tableOr, conc):
        return map( lambda x: [x,conc] ,tableOr)
        
    tmp = map(lambda x: incConclusion(x[0], x[1]), tmp)
    tmp = sum(tmp,[])
    #for x in tmp: print "lub", x[0], "  def" , x[1]
    return tmp

def carineFormRes(theory):
    
    
    tmp = resolutionForm(theory)
    st = ""
    for x in tmp: 
        st += "|".join( map( lambda x: " "+ x.prt(spec=1) + " ", x[0])) + "\n"
    return st


def instantineFormula(formula, consts):
        variables = formula.getVariables()
        if variables == []:
            return [formula]
        
        formulas = map(lambda x: deepcopy(formula), range(len(consts)) )
        for x in xrange(len(consts)):
            formulas[x].substitute(variables[0],consts[x])
        
        return formulas

def instantine(theory, consts=[]):
    
        if consts==[]:
            consts = list(set(sum(map(lambda x:x.getConsts(), theory),[])))
              
        rest = theory
        nextRest = []
        
        while True:
            for x in rest:
                nextRest += instantineFormula(x,consts)
            if (nextRest == rest):
                break
            rest = nextRest;
            nextRest=[]
        
        return rest


class Theory:
#    __slots__ =('facts', 'rules','defaults', )

    _th_id =0        
    
    def __init__(self, file=None, db=None):
        self.ThFile = file
        self.theory = []
        self._theory = []
        self._th_id = self.__class__._th_id
        self.__class__._th_id +=1
        if file:
            try :
                self.theory = sents_parse(file,self._th_id)
                self._theory = self.theory
            except IOError as ins:
                print ins
        
        
        
    def save(self,file=None, db =None):
        if not file:
            file = self.ThFile
        f = open(file,"w")
        try:
            for x in self.theory:
                f.write(x.prt() + "\n")
        except IOError as ins:
            print ins
    
    def hasModel(self):
        pass
    
    
    

         
        
    def normalize(self):
        self.instantine()
        return  normalize(self.theory) 
        
    def convertToCNF(self):
        self.instantine()
        return convertToCNF(self.theory)
            
    def carineFormRes(self):
        self.instantine()
        return carineFormRes(self.theory)
        
    def resolutionForm(self):
        self.instantine()
        return resolutionForm(self.theory) 
    
    def instantine(self):
        self.theory = instantine(self.theory)
    
    def prepareGoal(self,goal):
        def extractConsts(listOfformulas):
            return list(set(sum(map( lambda x:x.getConsts() , listOfformulas),[])))
        
        self.theory = self._theory
      
        if not isinstance(goal, Formula):
            goal = self._addFormORDef(goal, 1, "parsing goal")
            
        goalConst = extractConsts(goal)
        
        theoryConsts = extractConsts(self.theory)
        
        self.theory = instantine(self.theory,theoryConsts + goalConst )
         
                
        goal = instantine(goal, goalConst+theoryConsts)
        
        goal = map(lambda x: x.negFormula(), goal)
        
        goal = resolutionForm(goal)
        
        return goal
    
    def setLinerResolution(self,goal, tab_proof):
        
        goal = self.prepareGoal(goal)
        
        self.iter = resolution.resolution.linearResolution(goal,self.resolutionForm(),10, tab_proof)
           
        
    def nextLinearResolution(self):
        return self.iter.next(), self.tabProof
        
    def carineReason(self, goal):
        if not isinstance(goal, Formula):
            goal = self._addFormORDef(goal, 1, "parsing goal")[0]
        
        s1 = self.carineFormRes()
        s2 = carineFormRes(goal.negFormula())
        return s1 +"\nnegated_conclusion\n"+s2
    
    def _addFormORDef(self, th, isFOFormula, errorStr):
        if type(th) == type(''):
            try:
                th = sents_parse_string(th,self._th_id)
            except SyntaxError as se:
                print se
                return
        if type(th) != type([]):
            th = [th]
        if len( filter( lambda x:x.FOformula ==isFOFormula, th ) ) != len(th):
            raise Exception(errorStr)
        return th
        
    
    def addFormula(self,formula):
       self.theory += self._addFormORDef( formula, 1, "not an First Order Formula")
    
    
    def addDefault(self,default):
        self.theory +=self._addFormORDef( default, 0, "not an Default")   
        
    def runCarrine(self,goal):
        th = self.carineReason( goal)
        file = "/home/kacper/studia/INF/Wnioskowanie/carine_072/th.t"
        ags  = ["/home/kacper/studia/INF/Wnioskowanie/carine_072/carine",file,"op=off", "xo=off"]
        file_object = open(file, 'w')
            
        file_object.write(th)
        file_object.close()
            
        p = subprocess.Popen(ags
                         , stdout = subprocess.PIPE, stderr =  subprocess.PIPE);

        p.wait()
        
        comm =  p.communicate()
        #print str(comm)
        if str(comm).find("Congratulations!!!")>=0:
            return True
        return False
        
        
    def toGoal(self,andTab):
        '''
        [ [x(a,b)], [] ]
        [[],[]]
        '''
        andTab = filter(lambda x: x!=[], andTab)
        if not andTab: return "" 
        tmp =[]
        for x in andTab:
            x = map(lambda u: str(u),x)
            tmp.append("||".join(x))
        tmp = "&&".join(tmp)
        print tmp
        return tmp
        
    def isOptymistic(self, formula, nr=10):
       # print "is opt"
        tab = []
        self.setLinerResolution(formula,tab)
        tmp = self.iter.next()
        
        
        if tmp == [] : return True
        print tab
        print tmp
       
            
            
        nextGoal = self.toGoal(tmp);
        if nextGoal == "":return True
        if nr :
            return self.isOptymistic(nextGoal, nr-1)
            
        
        return False
                

  
        

class SafeTheory:
    pass
            